(declare-fun _substvar_62_ () Bool)
(declare-fun _substvar_77_ () (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))
(declare-fun _substvar_109_ () Int)
(declare-const arr--85734156740198644_-85734156740198644-0 (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool)))))))))
(declare-const arr-5039030562382255027_-7952498975998772890-0 (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))))
(declare-const arr-3157953691764585969_1111476187209609344-0 (Array (Array (Array (Array Int Bool) Bool) (Array (Array (Array Int (Array Int Int)) (Array Int Int)) (Array (Array Int (Array Int Int)) (Array Int Int)))) (Array (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))) (Array (Array (Array (Array Bool (Array Bool Bool)) (Array Bool (Array Bool Bool))) (Array Int (Array Int Int))) (Array (Array (Array Bool (Array Bool Bool)) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))) (Array (Array Int Bool) (Array (Array Int Int) (Array Bool (Array Bool (Array Bool Bool))))))))))
(assert (xor true true (distinct 237 (abs _substvar_109_)) _substvar_62_ true true))
(assert (= _substvar_77_ arr-3157953691764585969_1111476187209609344-0 (store arr-3157953691764585969_1111476187209609344-0 arr-5039030562382255027_-7952498975998772890-0 arr--85734156740198644_-85734156740198644-0)))
(check-sat)
